Inductive even: nat -> Prop :=
  | even_0 : even O
  | even_SS :
      forall n:nat, even n -> even (S (S n)).

Lemma two_is_even:
  even (S (S O)).
Proof.
  constructor.
  constructor.
Qed.